A:msga{i:l}.
atom-free-decl{i:l}
atom-free-decl(Id; IdDeq; ds(A))
 atom-free-decl{i:l}
 atom-free-decl(Knd; KindDeq; da(A))
 AtomFree(Type{i'};ma-shape{i:l}
 AtomFree(Type{i'};ma-shape(A)) 

latex

Definitions

t  T, x:A. B(x), xdom(f). v=f(x)   P(x;v), f(a), x.A(x), nat-deq-aux, <a,b>, NatDeq, atom-deq-aux, AtomDeq, #$n, a<b, Void, False, x:AB(x), P  Q, A, AB, , {x:A| B(x) }, , Atom, prod-deq(A;B;a;b), proddeq(a;b), product-deq(A;B;a;b), IdLnkDeq, x:AB(x), IdLnk, sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), left+right, EqDecider(T), da(M), ds(M), Shape(M), State(ds), MsgA, AtomFree(d), KindDeq, Type, Knd, a:A fp B(a), AtomFree(T;x), IdDeq, Id, x. t(x), MsgA(ds;da), type List

Lemmas

msga-body wf, fpf wf, ma da wf, atom-free-decl wf, ma ds wf, msga wf, id-deq wf, Id wf, atom-free-Id, atom-free-fpf, Kind-deq wf, Knd wf, atom-free-Knd